Nuprl Lemma : es-le-not-locl 0,22

es:ES, ee':E. loc(e) = loc(e' Id  (e  e'   (e' <loc e)) 
latex


DefinitionsP  Q, P & Q, P  Q, False, P  Q, e  e' , A, (e <loc e'), Prop, Id, loc(e), E, x:AB(x), t  T, ES, P  Q, Trans x,y:TE(x;y), {T}
Lemmases-axioms, es-locl-antireflexive, es-locl-trans, event system wf, es-E wf, es-loc wf, Id wf, es-locl wf, not wf, es-le wf

origin